(* $Id: xCoreNormalizeFormula.ml 74 2007-10-16 12:20:18Z yann.regisgianas $ *)

open XCoreSyntax
open XCoreSyntaxExt

exception NotRedex

let rec beta_reduce f args =
  match f.fvalue with

    | FForallTys abs ->
	let (vs, body) = open_fforalltys_abs abs in
	  mk_lformula f.fpos 
	    (FForallTys (create_fforalltys_abs (vs, beta_reduce body args)))

    | FLam abs ->
	let args = List.map (fun a -> a.fvalue) args in
	let (ins, body) = open_lfun_abs abs in
	let (xs, tys) = List.split ins in
	  if Misc.list_same_length ins args then
	    many_subst_formula 
	      (List.map2 (fun (x, _) a -> (x, a)) ins args) body
	  else 
	    (match args with
	       | [ FProd args ] ->
		   beta_reduce f args
	       | [ v ] ->
		   let ty = mk_fprod_type tys in
		   let xs = List.map (fun x -> FVar x) xs in
		     mk_lformula f.fpos 
		       (mk_lforall f.fpos ins 
			  (mk_fimply f.fpos 
			     (mk_feq f.fpos ty v (mk_fprod f.fpos xs))
			     body.fvalue))
	       | _ -> assert false)

    | FPrimitive Pre ->
	(match args with
	   | [ p ] -> (match remove_fannot p.fvalue with FProd [ t1; t2 ] -> t1 
			 | _ -> raise NotRedex)
	   | _ -> raise NotRedex)

    | FPrimitive Post ->
	(match args with
	   | [ p ] -> (match remove_fannot p.fvalue with FProd [ t1; t2 ] -> t2
			 | _ -> raise NotRedex)
	   | _ -> raise NotRedex)

    | FAnnot (f, _) ->
	beta_reduce f args

    | _ -> 
	raise NotRedex

(** Implement LMOM evaluation strategy. *)

class normalizer = object (self)

  inherit map

  method fapp (f, args) =
    let f = remove_fannot' f in
    let nf = self#lformula f in
    let nargs = List.map self#lformula args in
      try (beta_reduce nf nargs).fvalue 
      with NotRedex -> FApp (nf, nargs)

  method flam abs = 
    let (ins, f) = open_lfun_abs abs in
      FLam (create_lfun_abs (ins, self#lformula f))

end

let normalize f = 
  (new normalizer)#formula f

let lnormalize f = 
  mk_lformula f.fpos (normalize f.fvalue)
